1. $T_{1}$ : Type
\\[0ex]2. $T_{2}$ : Type
\\[0ex]3. $T_{1}$ List
\\[0ex]4. $u$ : $T_{1}$
\\[0ex]5. $v$ : $T_{1}$ List
\\[0ex]6. $\forall$${\it bs}$:($T_{2}$ List). zip($v$;${\it bs}$) $\in$ ((:$T_{1}$ $\times$ $T_{2}$) List)
\\[0ex]7. $T_{2}$ List
\\[0ex]8. $T_{2}$
\\[0ex]9. $v_{1}$ : $T_{2}$ List
\\[0ex]10. rec{-}case($v_{1}$) of [] =$>$ [] $\mid$ $b$::${\it bs'}$ =$>$ .[$<$$u$, $b$$>$ / zip($v$;${\it bs'}$)] $\in$ ((:$T_{1}$ $\times$ $T_{2}$) List)
\\[0ex]$\vdash$  zip($v$;$v_{1}$) $\in$ ((:$T_{1}$ $\times$ $T_{2}$) List)